% \documentclass[11pt,compress]{beamer}
 \documentclass[11pt,compress,handout]{beamer}

%\usepackage{pgfpages}
%\setbeameroption{show notes}
%\setbeameroption{show notes on second screen=right}
\usepackage[utf8]{inputenc}
\usepackage{amsmath,amssymb,amsthm, amsfonts} 
\usepackage{mathpartir}
\usepackage{textcomp}
\usepackage{stmaryrd}
\usepackage{myproof}

\newcommand{\nopen}[2]{\mathsf{open}\,#1\,(#2)}
\newcommand{\open}[1]{\mathsf{open}(#1)}
\newcommand{\close}[1]{\mathsf{close}\langle#1\rangle}

\newcommand{\restr}[2]{(\nu #1 )#2}

\newcommand{\ifte}[3]{\mathsf{if}~ #1 ~\mathsf{then}~ #2 ~\mathsf{ else }~#3}

\newcommand{\branch}[2]{#1\triangleright \{#2\}}
\newcommand{\select}[2]{#1\triangleleft #2}

\newcommand{\rec}[2]{\mathrm{rec} (#1).#2}
\newcommand{\qua}{\ensuremath{\mathsf{q}}}  % 
\newcommand{\sepr}{ \  \mid \ }
\newcommand{\updated}[5]{{#1}^{#3}_{#4}\{#5(\mathsf{#2})\} } % a{P}
\newcommand{\inC}[2]{#1(#2)}  % output
\newcommand{\outC}[2]{\overline{#1}\langle #2 \rangle}  % output
\newcommand{\throw}[2]{{#1}!(#2)}  % throw
\newcommand{\catch}[2]{{#1}?(#2)}  % throw
\newcommand{\component}[4]{#1^#2 [#4]   }  %a^n[P]
\newcommand{\componente}[2]{#1[#2]   }  %a^n[P]
\newcommand{\update}[3]{{#1}\{#2(#3)\} } % a{P}
\def\sub#1#2{\{\raisebox{.5ex}{\small$#1$}\! / \mbox{\small$#2$}\}} %substitution
\newcommand{\intf}[1]{\Delta_{[#1]}}
\newcommand{\compat}{\ensuremath{\asymp}}  % 
%\newcommand{\nm}[1]{\ensuremath{\mathsf{#1}}}
% \newcommand{\nmu}[1]{\ensuremath{\mathtt{#1}}}
\newcommand{\componentbig}[2]{#1 \bigg[ #2 \bigg]   }  %a[P]
\newcommand{\componentbbig}[2]{#1 \big[ #2 \big]   }  %a[P]
\newcommand{\mupdate}[4]{{#1}^{#3}_{#4}\big\{#2\big\}} % a{P}
\newcommand{\capab}{\kappa}


\newcommand{\env}[2]{#1 \,;\, #2}
\newcommand{\type}[2]{#1;#2}
\newcommand{\judgement}[5]{\env{#1}{#2} \vdash #3 :: \type{#4}{#5}}
\newcommand{\judgebis}[3]{#1 \vdash #2 :: #3}






%\usepackage{japerez}
% Davides's macro
\usepackage{davidemacro}
%\usepackage{evolvablemacro}

%\usepackage[latin1]{inputenc}
%\usepackage[T1]{fontenc}
%\usepackage{pgfpages}

%\usepackage{times}
\usepackage{xspace}

\usepackage[english]{babel}
\usepackage{url}

\usepackage{wrapfig}

\hypersetup{%
	pdftitle={Adaptable Processes},%
	pdfauthor={Jorge A. Perez},%
	pdfsubject={},%
	pdfkeywords={process calculi, concurrency}%
}

\usepackage{color}
%\newcommand{\emphcolor}[1]{\textcolor{orange}{#1}\xspace}
\newcommand{\emphcolor}[1]{\textcolor{purple}{#1}\xspace}
\newcommand{\emphcolorb}[1]{\textcolor{blue}{#1}\xspace}
\newcommand{\emphcolorm}[1]{\textcolor{magenta}{#1}\xspace}

\newcommand{\whitecolor}[1]{\textcolor{white}{#1}\xspace}
\newcommand{\hidecolor}[1]{\textcolor{darkgray}{#1}\xspace}
\newcommand{\olivecolor}[1]{\textcolor{olive}{#1}\xspace}

%red, gray,
%orange,
%green, white, pink,
%blue, darkgray,
%cyan,	magenta,	yellow,	black, lightgray,	brown,	lime,	olive,
%purple,

\newcommand{\tealtext}[1]{\textcolor{teal}{#1}\xspace}

\newcommand{\str}[1]{\structure{#1}}


%\def\sub#1#2{\{\raisebox{.5ex}{\small$#1$}\! / \mbox{\small$#2$}\}}
%\newcommand{\til}[1]{\widetilde{#1}}
%\newcommand{\update}[2]{\til{#1}\{#2\} } 
%\newcommand{\component}[2]{#1 [#2]   }  %a[P]
%\newcommand{\outC}[1]{\overline{#1}}      % CCS  output

\newcommand{\bi}{\begin{itemize}}
\newcommand{\ei}{\end{itemize}}
\newcommand{\be}{\begin{enumerate}}
\newcommand{\ee}{\end{enumerate}}
\newcommand{\bbl}[1]{\begin{block}{#1}}
\newcommand{\ebl}{\end{block}}

\newcommand{\notas}[1]{\hidecolor{{\footnotesize {[#1]}}}}
\newcommand{\notass}[1]{\hidecolor{{\footnotesize {#1}}}}

% Context
\newcommand{\ol}{\langle\!\langle}
\newcommand{\cl}{\rangle\!\rangle}
\newcommand{\hl}[1]{\ol #1 \cl}
\newcommand{\fillcon}[2]{\ensuremath{#1\hl{#2}}}

\newcommand{\pired}{\longrightarrow}
\newcommand{\arro}[1]{\xrightarrow[]{#1}}

\newcommand{\rulename}[1]{\textsc{(#1)}}

\newcommand{\nm}[1]{\ensuremath{\mathsf{#1}}}
 \newcommand{\nmu}[1]{\ensuremath{\mathtt{#1}}}
 \newcommand{\midef}{\ensuremath{\stackrel{\mathsf{def}}{=}}}



%\newcommand{\str}[1]{\structure{#1}}
\newcommand{\fkspc}{{\tiny \ }\\}


\title[Session Types for Dynamically Evolvable Communicating Systems]{Session Types for Dynamically Evolvable Communicating Systems}
\author[Cinzia Di Giusto and Jorge A. P\'erez]{Cinzia Di Giusto  and \textbf{\emphcolor{Jorge A. P\'erez}}}
%\date[June 8, 2011]{GLOSS Seminar, FCUL - September 15, 2011}
\date{PLACES 2013}
  
\institute{\normalsize{University of Evry \\ \emphcolor{CITI - DI, New University of Lisbon}}}

\setbeamertemplate{navigation symbols}{} 

\usecolortheme{default}
%\useoutertheme{progressbar}
%\useinnertheme{progressbar}
%\usefonttheme{progressbar}

\usepackage{setspace}

\newcommand{\putat}[3]{\begin{picture}(0,0)(0,0)\put(#1,#2){#3}\end{picture}}

\begin{document}



\begin{frame}
%\progressbaroptions{titlepage=normal}

 \titlepage
\end{frame}


\section{Context and Motivation}

\frame{
\frametitle{Adaptation and Evolution}
Modern software systems and apps require \\
to \emphcolor{adapt} to their environment and \str{evolve} accordingly:
\bi
\item Enforce new requirements; enhance reliability
\item Implement maintenance or recovery policies
\item React to unexpected circumstances \\ (such as errors and user demand peaks) \pause
\ei
\notas{All of the above: as transparently as possible} \pause

\bigskip

A complex issue; many possible perspectives:
\bi
\item System infrastructures \notas{e.g. scaling in cloud computing}
\item Software architectures/paradigms \\ \notas{e.g. aspect-oriented and context-aware programming}
\item \str{Programming languages and models} \\ \notas{e.g. constructs for exceptions, compensations, reversibility}
\ei
}

\frame{
\frametitle{Adaptation and Evolution}

Still, widely studied models for concurrency are \str{not suited} to account for \emphcolorm{complex} forms of evolution/reconfiguration
\pause
\smallskip

\bi
\item Suspend, replace, modify portions of the system at runtime
\item Name passing is useful but only at a local (low) level
\item Global, atomic reconfiguration is difficult to express
\item Resulting models are contrived and/or hard to reason about
\ei

\bigskip

In particular, (typed) models of disciplined communications incorporate only limited forms of evolution/reconfiguration.

}

\frame{
\frametitle{This Work: Adaptation for Communicating Processes}


More flexible and open models of communicating systems by integrating rich and flexible
\str{built-in adaptation mechanisms} 

\smallskip

\begin{block}{Context}
Interacting partners (expressed as $\pi$-calculus processes) which execute
 communication protocols (enforced via session types)
\end{block}
%\vspace{-2mm}
\begin{block}{Goals}
\bi
\item \str{Integration of concerns:} Enforce communication correctness while admitting useful forms of runtime reconfiguration
\item \str{Conservativity:} Stay as close as possible to ``usual'' session-based frameworks  
\ei
\end{block}
%\vspace{-2mm}
\begin{block}{Main challenge}
Harmonize communication behavior and reconfiguration actions
\end{block}
}


\frame{
\frametitle{Our Choices} 
A synchronous $\pi$-calculus with \str{adaptable processes}
\bi
\item \str{Located processes} \\ Distinguished sites in which behavior resides 
\item \str{Update processes} \\ Adaptation functions which act on located processes
\ei

\bigskip

We build upon \emphcolorm{safe sessions} for Ambients \notas{Garralda et al.-PPDP'06}:
\bi
\item Binary session types \str{with delegation}
\item Processes spread over arbitrary (but explicit) domains
\item Prioritize communication over reconfiguration
\item Updates dependant on (basic) notions of interfaces/contracts %\\ \notas{used to enable/control reconfiguration}
\ei

\begin{block}{Results}
\bi
\item Session fidelity: Session types are respected along execution
\item Consistency: Update actions do not interrupt  active sections
\ei
\end{block}
}

\section{AP}




\frame{
\frametitle{Adaptable Processes (1)}
A process calculi approach to evolvable systems
\begin{itemize}
  \item Provide \emphcolor{direct control} on process execution 
  \item Processes can be stopped, restarted, relocated, at runtime 
  \item A form of \emphcolor{higher-order} process communication
\end{itemize}

\bigskip

Good knowledge on expressiveness, decidability, verification issues \\
\notas{cf. Works with  Bravetti and Zavattaro (FORTE'11, ISOLA'12, LMCS'12)}
}

\frame{
\frametitle{Adaptable Processes (2)}




Global, atomic runtime reconfiguration via two constructs:

\begin{itemize}
\item Located processes, written {\large $\componente{a}{P}$} \\ 
\emphcolor{(adaptable) process} $P$ is \emphcolor{located at} name $a$
\item Update process, written {\large $\update{a}{Q}{X}$} \\
$Q(X)$ is a \emphcolorb{context} with zero or more occurrences of \emphcolorb{variable} $X$
\end{itemize}

%\bigskip

\begin{block}{Informal (untyped) semantics:}

\bi
\item Located reconfiguration:
\large{ $$ \componente{a}{P} \parallel \update{a}{Q}{X} \longrightarrow Q\sub{P}{X}$$}

\item Transparent locations:
{\large $$ \text{if } P \longrightarrow Q \text{ then } \componente{a}{P}  \longrightarrow \componente{a}{Q}$$}

\ei
\end{block}

}

\frame{
\frametitle{A Session Language with APs (Excerpt)}

%In a session-typed context, the two constructs are annotated:
$$
\begin{array}{lclr}
P \!\!& \!\!::=  
	& \!\!\! \nopen{a}{c:\rho_\qua}.P  & \text{open session}	\\
	& \sepr & \!\!\!\outC{c}{\tilde{e}}.P & \text{data output}  \\
  	&\sepr &  \!\!\! \inC{c}{\tilde{x}}.P  & \text{data input} \\
	& \sepr & \!\!\!\throw{c}{d}.P & \text{channel output} \\
    &\sepr &  \!\!\!\catch{c}{d}.P  & \text{channel input} \vspace{1mm}\\
	&\sepr& \!\!\!\component{l}{h}{\Delta}{P} ~~(h \geq 0)  & \text{\emphcolor{adaptable process}}\vspace{1mm} \\
% &   & \sepr & \!\!\! \mathsf{X}& \text{process variable} \\
	&\sepr& \!\!\!\updated{l}{X}{\Delta_1}{\Delta_2}{P} & \text{\emphcolorb{update process}} \vspace{1mm}\\
%  	& \sepr & \!\!\!\ifte{e}{P}{Q} & \text{conditional}\\
%	    & \sepr & \!\!\! Y& \text{recursion variable}\\	 
%	& \sepr & \!\!\! \rec{Y{:}\Phi{\cdot}\Delta}{P}& \text{recursion}\\	
  	& \sepr & \!\!\! P \parallel P & \text{parallel}\\	 
%	&\sepr& \!\!\! \branch{c}{n_1:P_1, \ldots, n_k:P_k} & \text{branching}\\
%	&\sepr& \!\!\! \select{c}{n}.P & \text{selection}\\
		&\sepr& \!\!\! \close{c}.P & \text{close session}	\\
			&\sepr& \!\!\! \restr{u}{P}  & \text{name/channel hiding}	\\
			&\sepr& \!\!\! \mathbf{0}  & \text{inaction} %\\
%e	&::= & \!\!\! k &\text{constants} \\
%    & \sepr & \!\!\! e_1 + e_2 \sepr e_1 - e_2  \sepr \ldots & \text{operators}
\end{array} 
$$

Key annotations:
\bi
\item Association with session types is \emph{local}. %Explicit close construct. 
\item $h$: the number of open sessions at a given location
\item  $\Delta$: an interface (set of declared sessions)
\ei
}

\frame{
\frametitle{A Session Language with Adaptable Processes (2)}

$C, D, E$~: contexts which denote a structure of nested locations.\\
$C^{+}$, $C^{-}$~: modifications on the annotations of the locations in $C$.

$$
\begin{array}{c}
E\big[C[\nopen{a}{c:\rho_{\qua}}.P] \parallel D[\nopen{a}{d:\overline{\rho}_{\qua}}.Q]\big] \\
\pired  \\
 \restr{c'}{\big(E^{+}_{}\big[{C^{+}_{}[P\sub{c'}{c}] \parallel D^{+}_{}[Q\sub{c'}{d}]}\big]\big)} \vspace{5mm} \\
E\big[C[\throw{c}{d}.P] \parallel D[\catch{c}{d}.Q]\big] \pired E\big[C^{-}[P] \parallel D^{+}[Q]\big] 
 \vspace{5mm}\\
E\big[C[\component{l}{0}{}{Q}] \parallel D[\updated{l}{X}{\Delta_1}{\Delta_2}{P}]\big]~~ 
{\small \emphcolorb{(\text{with }\intf{Q} \compat\Delta_1)}} \\ \pired   \\
E_{}\big[C[P\sub{Q}{\mathsf{X}}] \parallel D[\nil]\big] \vspace{5mm}
\\
E\big[C[\close{c}.P] \parallel D[\close{c}.Q]\big] \pired  E^{-}\big[C^{-}[P] \parallel D^{-}[Q]\big]
\end{array}
$$


%Main highlights:
\bi
\item Session establishment enforces type duality %Location counters are increased. 
\item Reconfiguration depends on interface compatibility, noted $\compat$
\ei
}


\frame{
\frametitle{Example: A simple model of workflow adaptation (1)}
We may  abstract a workflow application as the following  process:
 $$
  App ~\triangleq~ \componentbig{\nm{wfa}^0}{\, \componentbbig{\nm{we}^0}{\nmu{WE} \parallel \nm{W}_{1} \parallel \cdots \parallel \nm{W}_{k} \parallel \component{\nm{\nm{wbl}}}{0}{}{\nmu{BL}}} \parallel \nmu{S}_{1} \parallel \cdots \parallel \nmu{S}_{j}\,}
 $$
 where the $i$-th workflow (two activities, located on names $\nm{r}$ and $\nm{t}$) is defined as:
 $$
%\nm{W}_{i} \triangleq \componentbig{\nm{w}_{i}^0}{\,  \nmu{WL}_{i} \parallel \prod_{j=1}^n  \component{\nm{a}_j}{0}{}{\nmu{P}_{j}}  \,}
\nm{W}_{i} \triangleq \componentbbig{\nm{w}_{i}^0}{\,  \nmu{WL}_{i} \parallel  \component{\nm{r}}{0}{}{\nmu{P}_{1}} \parallel  \component{\nm{t}}{0}{}{\nmu{P}_{2}} \,}
$$
%Suppose that $\nm{W}_{i}$ has two activities only, : $\nm{W}_{i} \triangleq \componentbbig{\nm{w}_{i}^0}{\,  \nmu{WL}_{i} \parallel  \component{\nm{r}}{0}{}{\nmu{P}_{1}} \parallel  \component{\nm{t}}{0}{}{\nmu{P}_{2}} \,},$ 

\smallskip

The activity located at $r$ defines a simple session-typed behavior: %with  $\nmu{P}_1$ defined as
\begin{eqnarray*}
\nmu{P}_1 \!\!& \!\!\triangleq \!\!& \nopen{a}{s:\sigma}.\inC{s}{u,p}.\select{s}{n_1.Q[s]}.\close{s} 
\end{eqnarray*}
}

\frame{
\frametitle{Example: A simple model of workflow adaptation (2)}
Recall 
 $$
\nm{W}_{i} \triangleq \componentbbig{\nm{w}_{i}^0}{\,  \emphcolor{\nmu{WL}_{i}} \parallel  \component{\nm{r}}{0}{}{\nmu{P}_{1}} \parallel  \component{\nm{t}}{0}{}{\nmu{P}_{2}} \,}
$$
Suppose $\emphcolor{\nmu{WL}_{i}}$ contains a \emphcolorb{reconfiguration policy} $Rec$ for $\nm{W}_{i}$: 
%for location $\nm{r}_{}$.
\begin{eqnarray*}
Rec & \triangleq &
\ifte{e}{\mupdate{\nm{r}}{\component{\nm{v} }{0}{}{\mathsf{X}}}{\sigma}{\sigma}}
{\mupdate{\nm{r} }{\component{\nm{r}_1 }{0}{}{\nmu{S'} }  \parallel \component{\nm{r}_2 }{0}{}{\nmu{S''} } }{\sigma}{\Delta}} \quad\text{where:} \\
\nmu{S'}  \!\!& \!\!\triangleq \!\!&\!\!\nopen{a}{s:\sigma}.\nopen{b}{d:!(\sigma)}.\throw{d}{s}.\close{d} \\
%\nmu{P'}  \!\!& \!\!\triangleq \!\!&\!\!\nopen{a}{s:\sigma}.\nopen{b}{d:!(\sigma)}.\throw{d}{s}.\close{d}.\close{s} \\
\nmu{S''}  \!\!& \!\!\triangleq \!\!& \!\!\nopen{b}{e:?(\sigma)}.\catch{e}{s}.\inC{s}{u,p}.\select{s}{n_1.Q[s]}.\close{s}.\close{e} \\
%\nmu{P''}  \!\!& \!\!\triangleq \!\!& \!\!\nopen{b}{e:?(\sigma)}.\catch{e}{s}.\inC{s}{u,p}.\select{s}{n_1.Q_1}.\close{e} 
%& & \text{($X$ does not appear in $S', S''$} 
\end{eqnarray*}
%represents a simple adaptation routine enforcing explicit distribution of interacting processes.

\pause
\bigskip
Runtime reconfiguration then depends on the boolean $e$. \\ % evaluates to:
If $e$ reduces to true then simply \emphcolorb{relocate} at $v$ the current behavior:
%Thus, $Rec$ formalizes a reconfiguration policy that depends on the boolean value $e$ evaluates to:
%if $e$ reduces to true, then the behavior at activity $\nm{r}$ will be kept unchanged, but it will be relocated to name $\nm{v}$:
$$
\nm{W}_{i} \pired^* \componentbbig{\nm{w}_{i}^0}{\, \component{\nm{v}}{0}{}{\nmu{P}_1}  \parallel \component{\nm{t}}{0}{}{\nmu{P}_{2}}  \,}
$$
Otherwise, if $e$ evaluates to false then \emphcolor{replace} current behavior with the delegation-based implementation defined by $Rec$:
%, an update action on $\nm{r} $will reconfigure the distributed structure of $\nmu{P}_1$:
\begin{equation*}
\nm{W}_{i} \pired^* \componentbbig{\nm{w}_{i}^0}{\, \component{\nm{r}_1}{0}{}{\nmu{S'}}  \parallel \component{\nm{r}_2}{0}{}{\nmu{S''}}  \parallel \ \component{\nm{t}}{0}{}{\nmu{P}_{2}}  \,} \label{eq:l}
\end{equation*}
%Thus, in a single step, 
%the monolithic service $\nmu{P}_1$ will be replaced with a more flexible 
%implementation in which $\nmu{P'} $ (located  at $\nm{r}_1$) first establishes a session and then \emph{delegates} it to $\nmu{P''} $ (located at $\nm{r}_2$).

}

\frame{
\frametitle{Type System: Syntax}
We have deliberately aimed at retaining a type structure close to standard session types presentations. 

\smallskip

Assuming a set of \emphcolor{basic types}, ranged over $\capab, \capab', \ldots$, we have:
$$
\begin{array}{lrl}
%\text{Basic types  } \capab & ::= & \mathsf{int} \sepr \mathsf{b ool} \sepr \dots ~~~ \\
\text{}\zeta & ::= & \epsilon  \!
		~\sepr~   !(\tilde{\capab}).\zeta 
		~\sepr~ ?(\tilde{\capab}).\zeta  
		~\sepr~   !(\sigma).\zeta 
		~\sepr~ ?(\sigma).\zeta \\
		&  \sepr& 
		   t 
		~\sepr~   \mu t.\zeta \\
	& \sepr & 	  \&\{n_1:\zeta_1, \dots,  n_k:\zeta_k \}   
		~\sepr~   \oplus\{n_1:\zeta_1, \dots , n_k:\zeta_k \}   \\ 
		& & \\
		\text{} \rho & \triangleq &  \{ \zeta ~|~ \mathsf{ftv}(\zeta) = \emptyset\} \\ & &  \\
%\text{Type Qualifiers  } \qua & ::= & \qual \sepr \quau  \! \\
\text{}\omega &::=& \rho_\qua \sepr 	\bot 
\end{array}
$$
}

\frame{
\frametitle{Type System: Judgments}

\begin{block}{Type judgment}
$$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi}{\Delta}} $$
Under environments $\Gamma$ and $\Theta$, 
process $P$ has active sessions declared in $\Phi$ and interface %(a collection of not yet open sessions) 
$\Delta$. 
\end{block}

\bi
\item Interfaces $\Delta$ are collections of closed pre-session types $\rho$. These represent available but not yet active sessions
%We also require a
\item Set~$\Phi$  collects information on already active sessions: it records 
a channel name  and its associated session type.
\item $\Gamma$ is a first-order env.: it maps expressions with basic types $\capab$
\item $\Theta$ is a higher-order env.: it  stores the type of process/recursion variables
\ei



}


\frame{
\frametitle{Type System: Key Typing Rules}
%We only present typing rules for adaptable and update processes; see~\cite{dGP13} for a full account.
Rule $\rulename{t:Loc}$ checks that the annotation for located processes corresponds to the number of open sessions:
$$
\begin{array}{lc}
\rulename{t:Loc} & \cfrac{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi}{\Delta}} \qquad h = \#\{c \mid c:\omega \in \Phi\} }{\judgebis{\env{\Gamma}{\Theta}}{\component{l}{h}{\Delta}{P} }{ \type{\Phi}{\Delta}}} \\
\end{array}
$$

\bigskip

Rule $\rulename{t:Upd}$ ensures that the annotations for update processes correspond to the interface of the variable involved,
and to that offered by the process:
$$
\begin{array}{lc}
\rulename{t:Upd}   & 
\cfrac{\judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\Delta_1}}}{P}{\type{\emptyset}{ \Delta_2 }}}{\judgebis{\env{\Gamma}{\Theta}}{\updated{l}{X}{\Delta_1}{\Delta_2}{P}}{\type{\emptyset}{ \emptyset}}}
\end{array}
$$

\begin{theorem}
Well-typedness is preserved by reduction.
\end{theorem}
 
}




\frame{
\frametitle{Consistency}
\bi
\item Process $P$ is said to be \emphcolor{communicating} over channel $c$
if it sends (resp. receives) a value/session on $c$, if it makes a selection (resp. offers a choice), or if 
it closes a session on $c$. 

\item Two communicating processes are \emphcolor{dual} on session $c$ if they are complementary to each other
%i.e., if one sends, the other receives on $c$; if one makes a selection, the other chooses; or if they are closing the same session $c$.
\item We write $Q_{\langle c \rangle}$ and $\overline{Q}_{\langle c \rangle}$ for dual comm. processes on $c$.

\item $\pired_r$ denotes a reduction originated from an update action
%an update action, i.e., a reduction inferred using rule $\rulename{r:Upd}$ 
%(possibly with the interplay of restriction/structural congruence rules).
%We say that %\begin{definition}[Consistency]\label{d:consist}%
\ei

A session on $c$ is \emphcolorb{consistent} in a process $P$ if,
for all $P', P''$ s.t. 
$$P \pired^{*} P' \equiv (\nu \tilde{u})\big (E\big[C[Q_{\langle c \rangle}] \parallel D[\overline{Q}_{\langle c \rangle}]\big] \big)$$
%where $R$ and $Q$ are dual communicating processes in that session, 
and $P' \pired_r P''$, then $\exists E', C', D'$ such that
$$P'' \equiv (\nu \tilde{u})\big (E'\big[C'[Q_{\langle c \rangle}] \parallel D'[\overline{Q}_{\langle c \rangle}]\big]\big)$$

}


\frame{
\frametitle{Con\-sist\-ency by Typing}
\begin{corollary}\label{cor:cons}
Suppose  
$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi}{\Delta}} $
is a well-typed process. \\
Then every session $\rho_\qua \in \Delta$ %that can be established along the evolution of $P$, we have that 
is consistent. %, in the sense of Def.~\ref{d:consist}.
\end{corollary}
}

\frame{
\frametitle{Ongoing and Future Work}
Many exciting directions!
\bi
\item Investigate stronger notions of correctness in the presence of adaptation (in particular, progress)
\item  Cast adaptable processes in other session types disciplines \\ (in particular, Giunti and Vasconcelos's)
\item  Refine notions of \\
\begin{center}
interface / interface compatibility / subtyping 
\end{center}
(as in work by, e.g., Castagna et al)
\ei
}

\begin{frame}
%\progressbaroptions{titlepage=normal}

 \titlepage
\end{frame}

\end{document}

\frame{
\frametitle{This talk in one slide}
\str{Adaptable processes}
\be
\item A \str{formal} model of  \emphcolor{evolvable} communicating processes \\
Processes can be discarded, stopped, relocated at runtime \pause 
\item Two \emphcolor{verification problems} for adaptable processes: \\
They describe bounded and unbounded \emphcolor{error repetition}   \pause 
\item Unfortunately, both problems are \emphcolor{undecidable}, so decision procedures for verification \emphcolor{do not exist} \pause
\item We investigate  \emphcolor{fragments} of adaptable processes where the problems 
are \emphcolor{decidable}
\ee
}

\begin{frame}
\frametitle{Roadmap}

\tableofcontents

\end{frame}

\AtBeginSection[]
{
  \begin{frame}
\setcounter{tocdepth}{3}
%\tableofcontents

      \frametitle{Roadmap}
      \tableofcontents[currentsection] 
  \end{frame}
}

\section{Motivation}

\begin{frame}
\frametitle{Context (very broad)}

Modern computing systems are increasingly
\begin{itemize}
\item \str{concurrent}
\begin{itemize}
\item multiple interacting entities, usually distributed \pause
\end{itemize}
\item \str{infinite} \pause
\begin{itemize}
\item termination is a \emphcolor{local} property
\item tolerant to \emphcolor{unexpected conditions} (e.g. failures) \pause 
\item but also able to \emphcolor{dynamically reconfigure} themselves \\ (e.g. performance and maintenance reasons)
\end{itemize}
\end{itemize}
\end{frame}


\frame{
\frametitle{The process calculi approach}
\begin{center}
%A \str{} to the analysis of \str{evolvable systems} 

%\pause

\bi
\item Identify some \str{phenomenon of interest} 
\item Isolate \str{basic construct(s)} for it, and define a \str{calculus}
\item Study the \str{properties} of the calculus (and systems modeled in it) and define \str{reasoning techniques} for it
\ei
\end{center}

%\pause

%We are mainly concerned with \emphcolor{dynamic reconfiguration} issues:\\
%\begin{itemize}
%\item finding proper \emphcolor{constructs} for representing evolution 
%\item defining \emphcolor{correctness properties} for evolvable systems
%\end{itemize}


%\pause
%
%\begin{block}{Our choices}
%\bi
%\item The phenomena: \str{components} and their \str{evolution}
%\item The calculus: $\mathcal{E}$, a core language with \str{updatable} components
%\item The properties: \str{(un)decidability} of component  \str{adaptation}
%\ei
%\end{block}

}

\frame{
\frametitle{Our base language: Milner's CCS}
\bi
\item CCS abstracts \str{concurrent  systems} into \\ \str{communicating processes} which interact via handshake 
\item It has been intensively studied in the last 10-20 years. \\ Many theoretical results
\bi 
\item behavioral equivalences 
\item logics 
\item \emphcolor{expressiveness and decidability}
\ei
 as well as software tools.
\item Together with the \str{$\pi$-calculus} (CCS's name-passing extension) are the most representative process calculi
\ei
}

\frame{
\frametitle{Our base language: Milner's CCS}

\str{Syntax.~} Assume an countable infinite collection of \str{names} $\mathcal{N}$, \\ and a complementary set of
\str{co-names} $\overline{\mathcal{N}} = \{\overline{a} \mid a \in \mathcal{N}\}$. \\
Let $\mathcal{L} = \mathcal{N} \cup \overline{\mathcal{N}}$ be a set of \str{prefixes}. %, and let $\mathcal{L} \cup \tau$ be the \str{actions}.
\pause
\vspace{0.2cm}
\[
\hspace{-6mm}
\begin{array}{rcll}
P,Q & :: = &  \sum_{i \in I} \pi_{i}.P_{i}    ~& \mbox{choice among all $\pi_{i}.P_{i}$ with $\pi_{i} \in \mathcal{L}$}\\[\mypt]
 & \midd &  P \parallel Q & \mbox{parallel composition (concurrency)} \\[\mypt]
 & \midd &  !\pi.P & \mbox{infinitely many copies of $P$ with trigger $\pi$} \\[\mypt]
 & \midd &  (\nu \til{n})P & \mbox{name restriction: $\til{n}$ are bound in $P$} 
\end{array} 
 \]
\pause
\vspace{0.4cm}

Two special cases of the choice operator: \\
~~~The \str{inactive} process  $\nil$ (when the sum is empty)\\
~~~The \str{binary choice} $\pi_{1}.P_{1} + \pi_{2}.P_{2}$ (when ${|}I{|}=2$).

Also, we write $\prod_{i \in I} P_{i}$ to abbreviate $P_{1} \parallel P_{2} \parallel \cdots \parallel P_{n}$
}

\frame{
\frametitle{Our base language: Milner's CCS}

\str{Operational Semantics.~} A Labeled Transition System (LTS)\\
Let $\mathcal{A} = \mathcal{L} \cup \tau$ be the set of \str{actions}.  Below, $\alpha \in \mathcal{A}$.

$$
\inferrule[]{}{\sum_{i\in I} \pi_i.P_i \arro{~\pi_j~}  P_j ~~(j \in I)}   
\qquad
\inferrule[]{}{!\pi.P \arro{~\pi~}  P \parallel !\pi.P }
$$
$$
\inferrule[]{P_1 \arro{~\alpha~} P_1'}{P_1 \parallel P_2 \arro{~\alpha~} P'_1 \parallel P_2}	
\quad
\inferrule[]{P \arro{~\alpha~} P' \andalso \alpha,\overline{\alpha} \text{ not in } \til{n}}{(\nu \til{n})P  \arro{~\alpha~}  (\nu \til{n})P'}
$$
$$
\fbox{
\inferrule[]{P_1 \arro{~a~} P_1' \andalso P_2 \arro{~\outC{a}~} P'_2}{P_1 \parallel P_2 \arro{~\tau~}  P'_1 \parallel P'_2}
}
$$
}

\frame{
\frametitle{Our base language: Milner's CCS}
\str{Example:~}A process which emits a  signal $\outC{e}$ infinitely  often:
\begin{eqnarray*}
%\hspace{-7mm}
S & = & \outC{s} \parallel !s.\outC{a} \parallel !a.\outC{e}.\outC{s}  \pause \qquad \text{[synchronize on $s$, release $\outC{a}$]} \\ 
& \arro{~\tau~} &   \outC{a} \parallel !s.\outC{a} \parallel !a.\outC{e}.\outC{s} \pause \qquad \text{[synchronize on $a$, release $\outC{e}.\outC{s}$]}  \\
& \arro{~\tau~} &  !s.\outC{a} \parallel \outC{e}.\outC{s} \parallel !a.\outC{e}.\outC{s} \pause \qquad \text{[emit output  on $e$]} \\
 & \arro{~\outC{e}~} & \outC{s} \parallel !s.\outC{a} \parallel !a.\outC{e}.\outC{s}  \\
& = & S 
\end{eqnarray*}
}

\frame{
\frametitle{The process calculi approach, \underline{in our case}}
\begin{center}
%A \str{} to the analysis of \str{evolvable systems} 

%\pause

\bi
\item Identify some \str{phenomenon of interest} 
\item Isolate \str{basic construct(s)} for it, and define a \str{calculus}
\item Study the \str{properties} of the calculus (and systems modeled in it) and define \str{reasoning techniques} for it
\ei
\end{center}

\pause

Here, we are concerned with \emphcolor{dynamic reconfiguration} issues:\\
\begin{itemize}
\item finding proper \emphcolor{constructs} for representing evolution 
\item defining \emphcolor{correctness properties} for evolvable systems
\end{itemize}


%\pause
%
%\begin{block}{Our choices}
%\bi
%\item The phenomena: \str{components} and their \str{evolution}
%\item The calculus: $\mathcal{E}$, a core language with \str{updatable} components
%\item The properties: \str{(un)decidability} of component  \str{adaptation}
%\ei
%\end{block}

}

\frame{
\frametitle{Dynamic reconfiguration is important}
It is everywhere:
\bi
\item Software update (in OS, for instance)
\item Runtime reconfiguration in component-based systems
\item Workflow applications
\item Cloud computing
\item Structured communication
\item \dots
\ei

\pause 
\fkspc
\emphcolorb{Claim:} Existing process calculi do not properly capture dynamic reconfiguration.
}

%\begin{frame}
%\frametitle{What is dynamic in known process calculi?}
%
%Essentially, the \emphcolor{underlying topology}: \pause 
%
%\begin{itemize}
%  \item CCS: interacting concurrent processes in a \str{static} topology
%  
%  \item The $\pi$-calculus: \str{dynamic communication} topologies through \emphcolor{channel/link mobility}
%%  \vspace{0.5cm}
%  
%  \item The Ambient calculus: \str{dynamic spatial} topologies through \emphcolor{ambient  mobility}
%  %(dynamic behaviours depending on the position)
%%\vspace{0.5cm}
%\end{itemize}
%
%
%%What about \emphcolor{dynamic reconfiguration}?
%%Dynamic reconfiguration does not really fit in any of these abstractions
%%  \item but what about dynamic behaviors? How to describe a process that changes along time?
%
%\end{frame}
%
%
%\begin{frame}
%\frametitle{What is dynamic in known process calculi?}
%Reconfiguration is only possible at a \emphcolor{low, local} level. \\ \pause
%In $\pi$-calculus, only the linkage structure can be reconfigured:
%\begin{center}
%\includegraphics[height=40mm]{linkmobility1.pdf}
%\end{center}
%\end{frame}
%
%\begin{frame}
%\frametitle{What is dynamic in known process calculi?}
%Reconfiguration is only possible at a \emphcolor{low, local} level. \\
%In $\pi$-calculus, only the linkage structure can be reconfigured:
%\begin{center}
%\includegraphics[height=40mm]{linkmobility2.pdf}
%\end{center}
%\end{frame}
%
%\begin{frame}
%\frametitle{What is dynamic in known process calculi?}
%Reconfiguration is only possible at a \emphcolor{low, local} level. \\
%In $\pi$-calculus, only the linkage structure can be reconfigured:
%\begin{center}
%\includegraphics[height=40mm]{linkmobility3.pdf}
%\end{center}
%\end{frame}
%
%\begin{frame}
%\frametitle{What is dynamic in known process calculi?}
%Reconfiguration is only possible at a \emphcolor{low, local} level. \\
%In $\pi$-calculus, only the linkage structure can be reconfigured:
%\begin{center}
%\includegraphics[height=40mm]{linkmobility4.pdf}
%\end{center}
%\end{frame}
%
%\begin{frame}
%\frametitle{What is dynamic in known process calculi?}
%Reconfiguration is only possible at a \emphcolor{low, local} level. \\
%In $\pi$-calculus, only the linkage structure can be reconfigured:
%\begin{center}
%\includegraphics[height=40mm]{linkmobility5.pdf}
%\end{center}
%\end{frame}
%
%\begin{frame}
%\frametitle{What is dynamic in known process calculi?}
%Reconfiguration is only possible at a \emphcolor{low, local} level. \\
%In $\pi$-calculus, only the linkage structure can be reconfigured:
%\begin{center}
%\includegraphics[height=40mm]{linkmobility6.pdf}
%\end{center} \pause
%What about \emphcolor{global} reconfiguration, performed \emphcolor{atomically}? \\
%(Say, relocating/replicating/hiding $P \parallel Q \parallel R$, \emphcolor{at once})
%\end{frame}




\section{Adaptable Processes}

\begin{frame}
\frametitle{Adaptable processes}
A process calculi approach to evolvable systems
\pause
\begin{itemize}
  \item Provide \emphcolor{direct control} on process execution 
  \item Processes can be stopped, restarted, relocated, at runtime 
  \item A form of \emphcolor{higher-order} process communication
\end{itemize}

\pause
\begin{block}{Our proposal}
\begin{enumerate}
\item A \emphcolor{process calculus} of adaptable processes, called \emphcolorb{\evol{}} \pause
\item \emphcolor{Verification problems} for evolvable systems defined in \evol{} \pause
\item \emphcolor{(Un)decidability results} for such problems
\end{enumerate}
\end{block}
\pause
In \str{this talk} I will  focus mainly on (1) and (2) 
\end{frame}

\begin{frame}
\frametitle{A calculus for adaptable processes }

\begin{block}{Syntax}
\visible<1,2,3,4>CCS without restriction \invisible<1>{plus \emphcolor{located processes}\\}\invisible<1,2>{ and \emphcolorb{update prefixes}:}
$$
\begin{array}{ll}
P        ::=& \sum_{i \in I} \pi_i.P_i   \, \midd \, 
          P \parallel P  \, \midd \, ! \pi.P \, \invisible<1>{\midd \, \emphcolor{\component{a}{P}}}\\ \\
\pi   ::=&  a \, \midd \, \outC{a} \invisible<1,2>{\, \midd \, \emphcolorb{\update{a}{U}}}
\end{array}
$$
\invisible<1,2,3>{where 
\begin{itemize}
\item $\component{a}{P}$ is the \emphcolor{adaptable process} $P$ \emphcolor{located at} name $a$
\item $U$ is a \emphcolorb{context}, with zero or more \emphcolorb{holes}, denoted $\bullet$
\end{itemize}}
\end{block}

\end{frame}








\begin{frame}
\frametitle{A calculus for adaptable processes}

\begin{block}{Operational Semantics: Intutions}
\begin{itemize}
\item Localities are \emphcolor{transparent}:
$$
 \rightinfer
 			{\component{a}{P} \xrightarrow{~\alpha~}  \component{a}{P'}}
 			{P \xrightarrow{~\alpha~} P'} 
			$$
			
\item Reconfiguration via \emphcolor{interaction}  with update prefixes:
$$
\component{a}{P} \parallel \update{a}{U}.Q \xrightarrow{~\tau~} \fillcon{U}{P} \parallel Q
$$
\pause 
\hspace{-6mm}
\small{[$\fillcon{U}{P}$ is the \emphcolor{process} obtained by filling in the holes in $U$ with $P$]}
%\item An update replaces an adaptable process with a
%new process filled with the process currently
%active in the updated location
%
%\end{itemize}
%
%metti sintassi di techrep
% $$
%\begin{array}{c}
% \component{a}{P} \xrightarrow{~\component{a}{P}~}  \star
%\qquad 
%\rightinfer
%			{P_1 \parallel P_2 \xrightarrow{~\tau~} P_1'\sub{ U \sub{Q}{\bullet}  }{\star} \parallel P_2'}
%			{P_1 \xrightarrow{~\component{a}{Q}~} P_1' \qquad P_2 \xrightarrow{~\update{a}{U}~} P_2'}
%\end{array}
%$$
\end{itemize}
\end{block}

\end{frame}

\frame{
\frametitle{A calculus for adaptable processes}
%\vspace{-4mm}
\begin{block}{Operational Semantics: LTS}
%\vspace{-6mm}
%A Labeled Transition System (LTS) which extends that of C
{\footnotesize
$$
% \mathrm{\textsc{Comp}}~~~\component{a}{P} \arro{~\component{a}{P}~}  \star
%\fbox{\inferrule[\rulename{Comp}]{}{\component{a}{P} \arro{~\component{a}{P}~}  \star}}
%\qquad 
%  \mathrm{\textsc{Upd}}~~~\update{a}{P_1}.P_2 \arro{\update{a}{P_1}}  P_2
%$$
%$$
\hidecolor{\inferrule[]{}{\sum_{i\in I} \alpha_i.P_i \arro{~\alpha_i~}  P_i } }
%\rightinfer	[\textsc{Rec}]
 %			{rec \,X.P \arro{\alpha} P}
 %			{P\sub{rec \, X.P}{X} \arro{\alpha} P'}
 %\quad
\qquad
\hidecolor{\inferrule[]{}{!\alpha.P \arro{~\alpha~}  P \parallel !\alpha.P }}
$$
$$
%\fbox{\inferrule[\rulename{Loc}]{P \arro{~\alpha~} P'}{\component{a}{P} \arro{~\alpha~}  \component{a}{P'}}}
%\quad 
\hidecolor{\inferrule[]{P_1 \arro{~\alpha~} P_1'}{P_1 \parallel P_2 \arro{~\alpha~} P'_1 \parallel P_2}	}
\quad
\hidecolor{\inferrule[]{P_1 \arro{~a~} P_1' \andalso P_2 \arro{~\outC{a}~} P'_2}{P_1 \parallel P_2 \arro{~\tau~}  P'_1 \parallel P'_2}}
$$
}
\pause
$$
\hspace{-8mm}
\fbox{
\inferrule[]{}{\component{a}{P} \arro{~\component{a}{P}~}  \star}
\quad  
\inferrule[]{P \arro{~\alpha~} P'}{\component{a}{P} \arro{~\alpha~}  \component{a}{P'}}
\quad~~
\inferrule[]{P_1 \arro{~\component{a}{\emphcolor{Q}}~} P_1'\andalso P_2 \arro{~\update{a}{\emphcolorb{U}}~} P_2' }{P_1 \parallel P_2 \arro{~\tau~} P_1'\sub{ \fillcon{\emphcolorb{U}}{\emphcolor{Q}}  }{\star} \parallel P_2'}~}
$$
\\ 
\hidecolor{[Reduction $\pired$ is defined as $\arro{~\tau~}$]}
\end{block}
}

\frame{
\frametitle{A first example}

A basic client-server scenario:  
\begin{eqnarray*}
C & = & \componentbbig{client}{\component{run}{P} \parallel \outC{upd}.Q} \\
S & = & \componentbbig{server}{upd.\update{run}{\component{run}{R \parallel old.\bullet}}.S} 
\end{eqnarray*}

\pause

We then have two interactions, first on \emphcolor{$upd$} then on \emphcolor{$run$}:
\begin{align*}
%P & \componentbbig{client}{\component{run}{P} \parallel \outC{upd}.C} \parallel \componentbbig{server}{upd.\update{run}{\component{run}{Q \parallel old.\bullet}}.S} \\ 
C \parallel S \pired ~ & \componentbbig{client}{\component{run}{\emphcolor{P}} \parallel  Q} \parallel \componentbbig{server}{\update{run}{\str{\component{run}{R \parallel old.\bullet}}}.S} \\ 
\pired ~ & \componentbbig{client}{\str{\component{run}{R \parallel old.\emphcolor{P}}} \parallel Q} \parallel \componentbbig{server}{S}
\end{align*}

}

\frame{
\frametitle{Some evolvability patterns}
\begin{description}
\item<1-3>[Replacement] $$\quad \component{a}{\emphcolor{Q}} \parallel \update{a}{\str{\component{a}{R}}}.S \pired \str{\component{a}{R}} \parallel S  ~~(\bullet \not \in R)$$ 
\item<2-3>[Destroyer]$$\quad \component{a}{\emphcolor{Q}} \parallel \update{a}{\str{R}}.S \pired \str{R} \parallel S  ~~(\bullet \not \in R)$$ 
\item<3>[Plug-in] $$\component{a}{\emphcolor{Q}} \parallel \update{a}{\str{\component{a}{c{.}\bullet +R}}}.\nil \pired \str{\component{a}{c{.}\emphcolor{Q} +\fillcon{R}{\emphcolor{Q}}}} \parallel \nil$$ 
\end{description}
}

\frame{
\frametitle{Some evolvability patterns}
\begin{description}
\item<1-3>[Renaming] $$\componentbbig{m}{\component{a}{\emphcolor{Q}}} \parallel \componentbbig{n}{\update{a}{\str{\component{b}{\bullet}}}.S} \pired \componentbbig{m}{\str{\component{b}{\emphcolor{Q}}}}\parallel \componentbbig{n}{S}$$
\item<2-3>[Backup] $$\component{a}{\emphcolor{Q}} \parallel \update{a}{\str{\component{a}{\bullet}} \parallel \str{\component{b}{\bullet}}}.S \pired \str{\component{a}{\emphcolor{Q}}} \parallel \str{\component{b}{\emphcolor{Q}}} \parallel S$$
\item<3>[Deep update] $$\hspace{-55pt}\componentbbig{a}{Q \parallel \component{b}{R \parallel \emphcolor{\component{c}{S_{1}}}\, }\, } \parallel \update{c}{\str{\component{d}{S_{2}}}}.\nil \pired \componentbbig{a}{Q \parallel \componentbbig{b}{R \parallel \str{\component{d}{S_{2}}}\, }\, } \parallel \nil $$
\end{description}
}

\section{A Compelling Example}
\begin{frame}
\frametitle{A compelling  example: workflow reconfiguration}
 
% \begin{block}{}
%A workflow  describes how  a 
%number of activities coordinate to achieve a particular task.

A \str{workflow-based application}  consisting of 
\begin{enumerate}
\item  a \emphcolor{workflow engine (we)}  with workflows $\nm{W}_{1},  \ldots,  \nm{W}_{k}$ running on top of it. Each $\nm{W}_{i}$ contains several \emphcolor{activities}.
\item a \emphcolor{workflow base library (wbl)} to  support  running activities.
\item  \emphcolor{runtime services} $\nmu{S}_{1}, \ldots,  \nmu{S}_{m}$ implementing things like, e.g., transaction handling and external communication. 
\end{enumerate}

\pause

\fkspc

In \evol{}, this scenario may be represented as:
 $$
  App \midef \componentbig{\nm{wfa}}{\, \componentbbig{\nm{we}}{\nmu{WE} \parallel \underbrace{\nm{W}_{1} \parallel \cdots \parallel \nm{W}_{k}}_{\text{$k$ workflows}} \parallel \component{\nm{\nm{wbl}}}{\nmu{BL}}} \parallel \prod_{l \in M}\nmu{S}_{l} \,}
 $$

\end{frame}

\begin{frame}
\frametitle{A compelling  example: workflow reconfiguration}

\str{Representing a single workflow}
\begin{itemize}
\item Each workflow $\nm{W}_{i}$ is an adaptable process $\nm{w}_{i}$
containing 
a process $\nmu{WL}_{i}$ (the \emphcolor{workflow's logic}) 
and 
$n$ \emphcolor{activities} 

\item Each activity is formalized as an adaptable process $\nm{a}_{j}$ 
and an \emphcolor{execution environment} $\nm{env}_{j}$:
%\todo{$ea_1$ stands for execution environment for $a_i$}
$$
\nm{W}_{i} = \componentbig{\nm{w}_{i}}{\,  \nmu{WL}_{i} \parallel \prod_{j=1}^n \underbrace{\big(\component{\nm{env}_j}{\nmu{P}_{j}} \parallel \componentbbig{\nm{a}_{j}}{ !u_j. \update{\nm{env}_j}{\component{\nm{env}_j}{\bullet \parallel \nmu{A}_{j}}}}\big) }_{\text{$j$-th activity}}\,}
%\nm{W}_{i} = \component{\nm{w}_{i}}{\,  \nmu{WL}_{i} \parallel \prod_{j=1}^n (\component{\nm{env}_j}{\nmu{P}_{j}} \parallel \component{\nm{a}_{j}}{ !u_j. \update{\nm{env}_j}{\component{\nm{env}_j}{\bullet \parallel \nmu{A}_{j}}}}) \,}
$$
\end{itemize}

\end{frame}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



\begin{frame}
\frametitle{A compelling  example: workflow reconfiguration}
%\vspace{-5mm}

%\emphcolor{Updating a single activity.~}
Let's specify the 
%We define 
%update actions on $\nm{a}_{j}$ to 
\emphcolor{update a single activity} within a workflow.
%model an update to the \emphcolor{reconfiguration mechanisms} for a single activity:
$$
\nm{W}_{i} = \componentbig{\nm{w}_{i}}{\,  \emphcolorm{\nmu{WL}_{i}} \parallel \prod_{j=1}^n \underbrace{\big(\component{\nm{env}_j}{\nmu{P}_{j}} \parallel \componentbbig{\nm{a}_{j}}{ !u_j. \update{\nm{env}_j}{\component{\nm{env}_j}{\bullet \parallel \nmu{A}_{j}}}}\big) }_{\text{$j$-th activity}}\,}
%\nm{W}_{i} = \component{\nm{w}_{i}}{\,  \nmu{WL}_{i} \parallel \prod_{j=1}^n (\component{\nm{env}_j}{\nmu{P}_{j}} \parallel \component{\nm{a}_{j}}{ !u_j. \update{\nm{env}_j}{\component{\nm{env}_j}{\bullet \parallel \nmu{A}_{j}}}}) \,}
$$
  \pause \\

%\fkspc

%An upgrade to the \emphcolor{reconfiguration mechanisms} of $\nm{W}_{i}$.
Suppose a process
$R_{1} = !\,\nm{replace}_{j}.\updatebig{\nm{a}_{j}}{\component{a_{j}}{!u_{j}.\update{\nm{env}_j}{\component{\nm{env}_j}{\bullet \parallel \str{\nmu{newA}_{j}}}}}}$ \underline{inside 
$\emphcolorm{\nmu{WL}_{i}}$}. 

\fkspc

Given an output  at $\nm{replace}_{j}$, we obtain: 
$$
\nm{W}_{i} \pired \componentbig{\nm{w}_{i}}{\,  \emphcolorm{\nmu{WL}_{i}} \parallel \prod_{j=1}^n \big(\component{\nm{env}_j}{\nmu{P}_{j}} \parallel \componentbbig{\nm{a}_{j}}{ !u_j. \update{\nm{env}_j}{\component{\nm{env}_j}{\bullet \parallel \str{\nmu{newA}_{j}}}}}\big) \,}
$$
\end{frame}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{frame}
\frametitle{A compelling  example: workflow reconfiguration}
Let's specify the 
\emphcolor{suspension of a whole workflow} running in the workflow engine.
%Given our basic model, we can model \emphcolor{workflow suspension}  inside the workflow engine.
$$
App \midef \componentbig{\nm{wfa}}{\, \componentbbig{\nm{we}}{\emphcolorm{\nmu{WE}} \parallel \underbrace{\component{\nm{w}_{1}}{\nmu{WF}_{1}} \parallel \cdots \parallel \emphcolorm{\component{\nm{w}_{k}}{\nmu{WF}_{k}}}}_{\text{$k$ workflows}}\parallel \component{\nm{\nm{wbl}}}{\nmu{BL}}} \parallel \prod_{l \in M} \nmu{S}_{l}}
 $$
 \pause
 
Suppose a  process \\
$
R_{2} = !\,\nm{suspend}_{k}.\updatebig{\nm{w}_{k}}{\str{\nm{go}_{k}.\component{\nm{w}_{k}}{\bullet}}}
$
 inside  \emphcolorm{\nmu{WE}}.

\pause 

\fkspc

Given an output at $\nm{suspend}_{i}$, 
$\component{\nm{w}_{k}}{\nmu{WF}_{k}}$ 
and $R_{2}$
may interact:
%$$\nm{resume}_{i}.\component{\nm{w}_{i}}{\nmu{WF}_{i}}$$
$$
\hspace{-7mm}
App \pired \componentbig{\nm{wfa}}{\, \componentbbig{\nm{we}}{\emphcolorm{\nmu{WE}} \parallel \underbrace{\component{\nm{w}_{1}}{\nmu{WF}_{1}} \parallel \cdots \parallel  \str{\nm{go}_{k}.\component{\nm{w}_{k}}{\emphcolorm{\nmu{WF}_{k}}}} }_{\text{$k$ workflows}}\parallel \component{\nm{\nm{wbl}}}{\nmu{BL}}} \parallel \prod_{l \in M} \nmu{S}_{l}}
 $$
%which can be reactivated at a later time.
\end{frame}



\section{Verification Problems}

\begin{frame}
\frametitle{Correctness in an evolvable scenario: Intuitions}
%Distinguish between \emphcolor{correct} and \emphcolor{error} states, using \emphcolor{observables} 
\includegraphics[height=50mm]{cluster0.pdf}
\end{frame}


\begin{frame}
\frametitle{Correctness in an evolvable scenario: Intuitions}
%Distinguish between \emphcolor{correct} and \emphcolor{error} states, using \emphcolor{observables}
\includegraphics[height=50mm]{cluster2.pdf}
\end{frame}


\begin{frame}
\frametitle{Correctness in an evolvable scenario: Intuitions}
%Distinguish between \emphcolor{correct} and \emphcolor{error} states, using \emphcolor{observables}
\includegraphics[height=50mm]{cluster1.pdf}
\end{frame}

\begin{frame}
\frametitle{Correctness in an evolvable scenario: Intuitions}
%Distinguish between \emphcolor{correct} and \emphcolor{error} states, using \emphcolor{observables}
\includegraphics[height=50mm]{cluster3.pdf}
\end{frame}

\begin{frame}
\frametitle{Correctness in an evolvable scenario: Intuitions}
%Distinguish between \emphcolor{correct} and \emphcolor{error} states, using \emphcolor{observables}
\includegraphics[height=50mm]{cluster4.pdf}
\end{frame}



\begin{frame}
%\progressbaroptions{titlepage=normal}

 \titlepage
\end{frame}

\end{document}